a:Id, T:Type, ds:x:Id fp Type, P:(State(ds)TProp), init:x:Id fp ds(x)?Void.
(with ds: ds init: initaction a:T precondition a(v) is P)  MsgA 

latex

Definitions	t  T, x:AB(x), x:A. B(x), S  T, Void, x:A. B(x), Top, locl(a), KindDeq, Knd, Valtype(da;k), Type, x : v, IdLnk, x.A(x), x. t(x), 2of(t), rcv(l,tg), Id, a:A fp B(a), Prop, State(ds), IdDeq, f(x)?z, type List, , x:AB(x), 1of(t), S  T, mk-ma, with ds: ds init: initaction a:T precondition a(v) is P
Lemmas	mk-ma wf, ma-valtype wf, fpf-single wf, pi1 wf, fpf-empty wf, fpf-cap wf, id-deq wf, ma-state wf, fpf wf, Id wf, fpf-cap-single, rcv wf, pi2 wf, IdLnk wf, fpf-cap-single1, Knd wf, Kind-deq wf, locl wf